/**
 * Copyright (c) 2011 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.test.javasyp.logic;

import static com.googlecode.syper.anno.Pred.ensures;

import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;
import com.googlecode.syper.anno.Invariant;
import com.googlecode.syper.anno.Old;
import com.googlecode.syper.anno.Pred;
import com.googlecode.syper.anno.Result;
import com.googlecode.syper.anno.ReturnExcl;
import com.googlecode.syper.anno.ReturnImm;

import edu.cmu.cs.crystal.annotations.FailingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * Makes sure that array contents referenced by objects passed into modifying
 * methods are invalidated. 
 * @author kevin
 * @since Apr 10, 2011
 */
@FailingTest(2)
@UseAnalyses("SymbolicChecker")
public class ArrayModFail implements Invariant {

	@Excl private int[] a;
	int t;
	
	public ArrayModFail() {
		a = new int[] {1, 2, 3};
		Pred.ensures(a != null & a.length == 3 & a[0] == 1);
	}
	
	@Excl private void mayModContents() { excl: a[0] = 5; }
	
	@ReturnExcl @Imm private int[] contents() {
		imm: {
			@Result @Excl(borrowed = false) final int[] result = Old.Arrays.copyOf(a);
			Pred.ensures(result != null & result != a & result.length == a.length
			& Pred.forall(0, result.length, new Pred.IntPred() {
				public boolean cond(int k) { return result[k] == a[k]; }
			}));
			return result;
		}
	}
	
	@ReturnImm @Imm(released = true) 
	private int[] getContents() { imm: {
		@Result @Imm final int[] result = a;
		ensures(result != null & result == a);
		return result;
	} }

	public static void testDeepCopy() {
		final @Excl ArrayModFail a = new ArrayModFail();
		@Imm final int[] old = a.contents();
		assert Pred.forall(0, old.length, new Pred.IntPred() {
			public boolean cond(int k) { return old[k] == a.a[k]; }
		});
		a.mayModContents();
		// this should fail as a.a contents may have changed
		assert Pred.exists(0, old.length, new Pred.IntPred() {
			public boolean cond(int k) { return old[k] == a.a[k]; }
		});
	}

	public static void testBorrowingGetter() {
		final @Excl ArrayModFail a = new ArrayModFail();
		@Imm final int[] old = Old.Arrays.copyOf(a.getContents());
		assert Pred.forall(0, old.length, new Pred.IntPred() {
			public boolean cond(int k) { return old[k] == a.a[k]; }
		});
		a.mayModContents();
		// this should fail as a.a contents may have changed
		assert Pred.exists(0, old.length, new Pred.IntPred() {
			public boolean cond(int k) { return old[k] == a.a[k]; }
		});
	}

	/* (non-Javadoc)
	 * @see com.googlecode.syper.anno.Invariant#inv()
	 */
	@Override
	public boolean inv() {
		return a != null;
	}
	
}
